T:Type, L1, L2:(T List), x, y:T. (x  L1)  (y  L2)  x before y  L1 @ L2 

latex

Definitions	t  T, x before y  l, P  Q, x:A. B(x), Y, as @ bs, P & Q, P  Q,
Lemmas	l member wf, member iff sublist, sublist append